a, b:, n:. ((a+(b * n)) rem n) = (a rem n) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), a  b  T , False, A, P  Q, A  B, i  j , P & Q, P  Q, P  Q, , , {T}, , S  T
Lemmas	nat wf, nat plus wf, ge wf, nat properties, lt to le rw, nat plus inc, mul preserves le, add functionality wrt le, le wf, rem rec case